w:World, e:E. first(e)  time(pred(e))<time(e) 

latex

Definitions	b, isl(x), w-pred(w;e), a<b, time(e), x.A(x), World, first(e), P  Q, P & Q, x:AB(x), x:AB(x), b, Dec(P), P  Q, left+right, E, Type, Unit, x:A. B(x), t  T, A, P  Q, False, <a,b>, n-m, #$n, ij, pred(e), i=j, false, isnull(a), a(i;t), Prop, , outl(x), Void, AB, s = t, , n+m, -n, True, 2of(t), x. t(x), {x:A| B(x) }, Id,
Lemmas	nat wf, Id wf, pi2 wf, false wf, true wf, le wf, w-pred-wf2, bool wf, w-a wf, w-isnull wf, eqff to assert, iff transitivity, eqtt to assert, eq int wf, assert of eq int, nat properties, ge wf, w-pred wf, unit wf, w-E wf, isl wf, decidable assert, assert wf, not wf, bnot wf, assert of bnot, not functionality wrt iff, world wf, first wf